Inference at * 1 3 1 0 1 1 
Iof proof for Lemma fincr wf:



1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
  zz, n:. (n < zz)  (P(n)) 

latex

 by D 0 

latex

 1: 

 1: 3. zz : 
 1:   n:. (n < zz)  (P(n))
 2: .....wf..... NILNIL

 2:     Type
 .

Definitions	Type, s = t, , f(a), a < b, x:AB(x), , x:A. B(x), P  Q, t  T
Lemmas	nat wf